$\forall$$R$:Realizer. R{-}discrete($R$) $\in$ ${\it ix}$::Id $\times$ Id fp$\rightarrow$ $\mathbb{B}$